perm filename OTM.PRO[BMP,SYS] blob
sn#639868 filedate 1982-02-06 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00008 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 ←PROVE.LEMMA(LT.PA.PA.x (INDUCTION)
C00018 00003 ←PROVE.LEMMA(LT.PB.ID (INDUCTION)
C00023 00004 ←PROVE.LEMMA(LT.ID.PB (INDUCTION)
C00028 00005 ←DEFN(LTE (X Y)
C00030 00006 ←DEFN(LT (X Y)
C00031 00007 ←DEFN(EQ (X Y)
C00033 00008 ←PROVE.LEMMA(LTE.BI (REWRITE)
C00047 ENDMK
C⊗;
←PROVE.LEMMA(LT.PA.PA.x (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)))
(LESSP (OTM.SIZE.2 (PA Y) (PA X))
(OTM.SIZE.2 X Y)))
NIL)
This formula can be simplified, using the abbreviations IMPLIES and
OTM.SIZE.2, to the goal:
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)))
(LESSP (PLUS (COUNT (OFIX (PA Y)))
(COUNT (OFIX (PA X))))
(PLUS (COUNT (OFIX X))
(COUNT (OFIX Y))))).
This simplifies, opening up the functions OZEROP, NOT, OR, and OFIX, to
four new conjectures:
Case 4. (IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(NOT (OTM Y)))
(LESSP (PLUS (COUNT (PA Y)) (COUNT (PA X)))
(PLUS (COUNT X)
(COUNT (QUOTE (1QUOTE OZERO)))))).
But this again simplifies, applying PA.NOTM, and opening up the
functions COUNT, EQUAL, and PLUS, to:
(IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(NOT (OTM Y)))
(LESSP (COUNT (PA X))
(PLUS (COUNT X) 0))).
Appealing to the lemma PA/PB.ELIM, replace X by (PHI Z V) to
eliminate (PA X) and (PB X). We use the type restriction lemma noted
when PA was introduced and the type restriction lemma noted when PB
was introduced to constrain the new variables. We must thus prove:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI Z V)
(QUOTE (1QUOTE OZERO))))
(NOT (OTM Y)))
(LESSP (COUNT Z)
(PLUS (COUNT (PHI Z V)) 0))),
which we further simplify, rewriting with COUNT.PHI and SUB1.ADD1,
and expanding the definitions of PLUS and LESSP, to:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (OTM Y))
(NOT (EQUAL (COUNT Z) 0)))
(LESSP (SUB1 (COUNT Z))
(PLUS (PLUS (COUNT Z) (COUNT V))
0))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(OTM Y))
(LESSP (PLUS (COUNT (PA Y)) (COUNT (PA X)))
(PLUS (COUNT X) (COUNT Y)))).
Applying the lemma PA/PB.ELIM, replace Y by (PHI Z V) to eliminate
(PA Y) and (PB Y). We employ the type restriction lemma noted when
PA was introduced and the type restriction lemma noted when PB was
introduced to constrain the new variables. We must thus prove two
new conjectures:
Case 3.2.
(IMPLIES (AND (EQUAL Y (QUOTE (1QUOTE OZERO)))
(NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(OTM Y))
(LESSP (PLUS (COUNT (PA Y)) (COUNT (PA X)))
(PLUS (COUNT X) (COUNT Y)))),
which further simplifies, expanding the definitions of OTM, PA,
COUNT, EQUAL, and PLUS, to:
(IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X))
(LESSP (COUNT (PA X))
(PLUS (COUNT X) 0))).
Appealing to the lemma PA/PB.ELIM, we now replace X by (PHI Z V) to
eliminate (PA X) and (PB X). We employ the type restriction lemma
noted when PA was introduced and the type restriction lemma noted
when PB was introduced to constrain the new variables. We must
thus prove:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI Z V)
(QUOTE (1QUOTE OZERO)))))
(LESSP (COUNT Z)
(PLUS (COUNT (PHI Z V)) 0))),
which we further simplify, applying COUNT.PHI and SUB1.ADD1, and
opening up the definitions of PLUS and LESSP, to:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (COUNT Z) 0)))
(LESSP (SUB1 (COUNT Z))
(PLUS (PLUS (COUNT Z) (COUNT V))
0))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI Z V)
(QUOTE (1QUOTE OZERO))))
(NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X))
(LESSP (PLUS (COUNT Z) (COUNT (PA X)))
(PLUS (COUNT X) (COUNT (PHI Z V))))).
This simplifies further, applying COUNT.PHI, to the conjecture:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X))
(LESSP (PLUS (COUNT Z) (COUNT (PA X)))
(PLUS (COUNT X)
(ADD1 (PLUS (COUNT Z) (COUNT V)))))).
Appealing to the lemma PA/PB.ELIM, replace X by (PHI W D) to
eliminate (PA X) and (PB X). We rely upon the type restriction
lemma noted when PA was introduced and the type restriction lemma
noted when PB was introduced to restrict the new variables. This
produces:
(IMPLIES (AND (OTM W)
(OTM D)
(OTM Z)
(OTM V)
(NOT (EQUAL (PHI W D)
(QUOTE (1QUOTE OZERO)))))
(LESSP (PLUS (COUNT Z) (COUNT W))
(PLUS (COUNT (PHI W D))
(ADD1 (PLUS (COUNT Z) (COUNT V)))))),
which further simplifies, applying COUNT.PHI and SUB1.ADD1, and
opening up PLUS and LESSP, to:
(IMPLIES (AND (OTM W)
(OTM D)
(OTM Z)
(OTM V)
(NOT (EQUAL (PLUS (COUNT Z) (COUNT W))
0)))
(LESSP (SUB1 (PLUS (COUNT Z) (COUNT W)))
(PLUS (PLUS (COUNT W) (COUNT D))
(ADD1 (PLUS (COUNT Z) (COUNT V)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (OTM X)))
(LESSP (PLUS (COUNT (PA Y)) (COUNT (PA X)))
(PLUS (COUNT (QUOTE (1QUOTE OZERO)))
(COUNT Y)))),
which again simplifies, applying PA.NOTM, and expanding the functions
COUNT, EQUAL, and PLUS, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (OTM X)))
(LESSP (PLUS (COUNT (PA Y)) 0)
(COUNT Y))).
Appealing to the lemma PA/PB.ELIM, we now replace Y by (PHI Z V) to
eliminate (PA Y) and (PB Y). We employ the type restriction lemma
noted when PA was introduced and the type restriction lemma noted
when PB was introduced to constrain the new variables. This produces:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI Z V)
(QUOTE (1QUOTE OZERO))))
(NOT (OTM X)))
(LESSP (PLUS (COUNT Z) 0)
(COUNT (PHI Z V)))),
which we further simplify, applying COUNT.PHI and SUB1.ADD1, and
expanding the function LESSP, to:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (OTM X))
(NOT (EQUAL (PLUS (COUNT Z) 0) 0)))
(LESSP (SUB1 (PLUS (COUNT Z) 0))
(PLUS (COUNT Z) (COUNT V)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(OTM X))
(LESSP (PLUS (COUNT (PA Y)) (COUNT (PA X)))
(PLUS (COUNT X) (COUNT Y)))).
Appealing to the lemma PA/PB.ELIM, replace Y by (PHI Z V) to
eliminate (PA Y) and (PB Y). We rely upon the type restriction lemma
noted when PA was introduced and the type restriction lemma noted
when PB was introduced to constrain the new variables. This produces:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI Z V)
(QUOTE (1QUOTE OZERO))))
(OTM X))
(LESSP (PLUS (COUNT Z) (COUNT (PA X)))
(PLUS (COUNT X) (COUNT (PHI Z V))))).
But this simplifies further, applying COUNT.PHI, to:
(IMPLIES (AND (OTM Z) (OTM V) (OTM X))
(LESSP (PLUS (COUNT Z) (COUNT (PA X)))
(PLUS (COUNT X)
(ADD1 (PLUS (COUNT Z) (COUNT V)))))).
Applying the lemma PA/PB.ELIM, we now replace X by (PHI W D) to
eliminate (PA X) and (PB X). We rely upon the type restriction lemma
noted when PA was introduced and the type restriction lemma noted
when PB was introduced to restrict the new variables. This produces
the following two new conjectures:
Case 1.2.
(IMPLIES (AND (EQUAL X (QUOTE (1QUOTE OZERO)))
(OTM Z)
(OTM V)
(OTM X))
(LESSP (PLUS (COUNT Z) (COUNT (PA X)))
(PLUS (COUNT X)
(ADD1 (PLUS (COUNT Z) (COUNT V)))))).
This further simplifies, expanding the definitions of OTM, PA, and
COUNT, to:
(IMPLIES (AND (OTM Z) (OTM V))
(LESSP (PLUS (COUNT Z) 0)
(PLUS 0
(ADD1 (PLUS (COUNT Z) (COUNT V)))))),
which we again simplify, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (OTM W)
(OTM D)
(NOT (EQUAL (PHI W D)
(QUOTE (1QUOTE OZERO))))
(OTM Z)
(OTM V))
(LESSP (PLUS (COUNT Z) (COUNT W))
(PLUS (COUNT (PHI W D))
(ADD1 (PLUS (COUNT Z) (COUNT V)))))).
This simplifies further, applying COUNT.PHI and SUB1.ADD1, and
expanding the functions PLUS and LESSP, to the new formula:
(IMPLIES (AND (OTM W)
(OTM D)
(OTM Z)
(OTM V)
(NOT (EQUAL (PLUS (COUNT Z) (COUNT W))
0)))
(LESSP (SUB1 (PLUS (COUNT Z) (COUNT W)))
(PLUS (PLUS (COUNT W) (COUNT D))
(ADD1 (PLUS (COUNT Z) (COUNT V)))))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[14746 cns / 10.6 s + 2.6 gc + 5.9 io (= 22 @ 0)]
LT.PA.PA.x
←PROVE.LEMMA(LT.PB.ID (INDUCTION)
(IMPLIES (NOT (OZEROP X))
(LESSP (OTM.SIZE.2 (PB X) Y)
(OTM.SIZE.2 X Y)))
NIL)
This formula can be simplified, using the abbreviations OZEROP, NOT,
IMPLIES, and OTM.SIZE.2, to:
(IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X))
(LESSP (PLUS (COUNT (OFIX (PB X)))
(COUNT (OFIX Y)))
(PLUS (COUNT (OFIX X))
(COUNT (OFIX Y))))),
which simplifies, expanding the function OFIX, to two new conjectures:
Case 2. (IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(NOT (OTM Y)))
(LESSP (PLUS (COUNT (PB X))
(COUNT (QUOTE (1QUOTE OZERO))))
(PLUS (COUNT X)
(COUNT (QUOTE (1QUOTE OZERO)))))),
which again simplifies, opening up the definition of COUNT, to:
(IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(NOT (OTM Y)))
(LESSP (PLUS (COUNT (PB X)) 0)
(PLUS (COUNT X) 0))).
Applying the lemma PA/PB.ELIM, we now replace X by (PHI V Z) to
eliminate (PB X) and (PA X). We employ the type restriction lemma
noted when PB was introduced and the type restriction lemma noted
when PA was introduced to restrict the new variables. We would thus
like to prove the new formula:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI V Z)
(QUOTE (1QUOTE OZERO))))
(NOT (OTM Y)))
(LESSP (PLUS (COUNT Z) 0)
(PLUS (COUNT (PHI V Z)) 0))).
But this simplifies further, rewriting with COUNT.PHI and SUB1.ADD1,
and expanding the definitions of PLUS and LESSP, to:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (OTM Y))
(NOT (EQUAL (PLUS (COUNT Z) 0) 0)))
(LESSP (SUB1 (PLUS (COUNT Z) 0))
(PLUS (PLUS (COUNT V) (COUNT Z))
0))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL X (QUOTE (1QUOTE OZERO))))
(OTM X)
(OTM Y))
(LESSP (PLUS (COUNT (PB X)) (COUNT Y))
(PLUS (COUNT X) (COUNT Y)))).
Applying the lemma PA/PB.ELIM, replace X by (PHI V Z) to eliminate
(PB X) and (PA X). We employ the type restriction lemma noted when
PB was introduced and the type restriction lemma noted when PA was
introduced to constrain the new variables. We must thus prove the
new goal:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI V Z)
(QUOTE (1QUOTE OZERO))))
(OTM Y))
(LESSP (PLUS (COUNT Z) (COUNT Y))
(PLUS (COUNT (PHI V Z)) (COUNT Y)))).
This simplifies further, rewriting with COUNT.PHI and SUB1.ADD1, and
unfolding the definitions of PLUS and LESSP, to:
(IMPLIES (AND (OTM Z)
(OTM V)
(OTM Y)
(NOT (EQUAL (PLUS (COUNT Z) (COUNT Y))
0)))
(LESSP (SUB1 (PLUS (COUNT Z) (COUNT Y)))
(PLUS (PLUS (COUNT V) (COUNT Z))
(COUNT Y)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[4895 cns / 3.5 s + 0.0 gc + 1.9 io (= 6 @ 0)]
LT.PB.ID
←PROVE.LEMMA(LT.ID.PB (INDUCTION)
(IMPLIES (NOT (OZEROP Y))
(LESSP (OTM.SIZE.2 X (PB Y))
(OTM.SIZE.2 X Y)))
NIL)
This formula can be simplified, using the abbreviations OZEROP, NOT,
IMPLIES, and OTM.SIZE.2, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y))
(LESSP (PLUS (COUNT (OFIX X))
(COUNT (OFIX (PB Y))))
(PLUS (COUNT (OFIX X))
(COUNT (OFIX Y))))),
which simplifies, expanding the function OFIX, to two new conjectures:
Case 2. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (OTM X)))
(LESSP (PLUS (COUNT (QUOTE (1QUOTE OZERO)))
(COUNT (PB Y)))
(PLUS (COUNT (QUOTE (1QUOTE OZERO)))
(COUNT Y)))),
which again simplifies, opening up the definitions of COUNT, EQUAL,
and PLUS, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (OTM X)))
(LESSP (COUNT (PB Y)) (COUNT Y))).
Applying the lemma PA/PB.ELIM, we now replace Y by (PHI V Z) to
eliminate (PB Y) and (PA Y). We employ the type restriction lemma
noted when PB was introduced and the type restriction lemma noted
when PA was introduced to restrict the new variables. We would thus
like to prove the new formula:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI V Z)
(QUOTE (1QUOTE OZERO))))
(NOT (OTM X)))
(LESSP (COUNT Z) (COUNT (PHI V Z)))).
But this simplifies further, rewriting with COUNT.PHI and SUB1.ADD1,
and expanding the definition of LESSP, to:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (OTM X))
(NOT (EQUAL (COUNT Z) 0)))
(LESSP (SUB1 (COUNT Z))
(PLUS (COUNT V) (COUNT Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(OTM X))
(LESSP (PLUS (COUNT X) (COUNT (PB Y)))
(PLUS (COUNT X) (COUNT Y)))).
Applying the lemma PA/PB.ELIM, replace Y by (PHI V Z) to eliminate
(PB Y) and (PA Y). We employ the type restriction lemma noted when
PB was introduced and the type restriction lemma noted when PA was
introduced to constrain the new variables. We must thus prove the
new goal:
(IMPLIES (AND (OTM Z)
(OTM V)
(NOT (EQUAL (PHI V Z)
(QUOTE (1QUOTE OZERO))))
(OTM X))
(LESSP (PLUS (COUNT X) (COUNT Z))
(PLUS (COUNT X) (COUNT (PHI V Z))))).
This simplifies further, rewriting with COUNT.PHI, to:
(IMPLIES (AND (OTM Z) (OTM V) (OTM X))
(LESSP (PLUS (COUNT X) (COUNT Z))
(PLUS (COUNT X)
(ADD1 (PLUS (COUNT V) (COUNT Z)))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[4256 cns / 3.3 s + 2.6 gc + 1.8 io (= 9 @ 0)]
LT.ID.PB
←DEFN(LTE (X Y)
(IF (OZEROP X)
T
(IF (OZEROP Y)
F
(IF (LTE (PA X) (PA Y))
(IF (LTE (PA Y) (PA X))
(LTE (PB X) (PB Y))
(LTE (PB X) Y))
(IF (LTE (PA Y) (PA X))
(LTE X (PB Y))
F))))
NIL)
The lemmas LT.PA.PA, LT.PA.PA.x, LT.PB.PB, LT.ID.PB, and LT.PB.ID,
together with the definition of OZEROP, establish that (OTM.SIZE.2 Y X)
goes down according to the well-founded function LESSP in each
recursive call. Hence, LTE is accepted under the definitional
principle. The definition of LTE can be justified in another way. The
lemmas LT.PA.PA, LT.PA.PA.x, LT.PB.PB, LT.PB.ID, and LT.ID.PB, and the
definition of OZEROP, inform us that (OTM.SIZE.2 X Y) goes down
according to the well-founded function LESSP in each recursive call.
Observe that (OR (FALSEP (LTE X Y)) (TRUEP (LTE X Y))) is a theorem.
[25974 cns / 13.9 s + 5.4 gc + .4 io (= 25 @ 0)]
LTE
←DEFN(LT (X Y)
(AND (LTE X Y) (NOT (LTE Y X)))
NIL)
Note that (OR (FALSEP (LT X Y)) (TRUEP (LT X Y))) is a theorem.
[937 cns / 1.2 s + 2.9 gc + .1 io (= 9 @ 0)]
LT
←DEFN(EQ (X Y)
(AND (LTE X Y) (LTE Y X))
NIL)
Note that (OR (FALSEP (EQ X Y)) (TRUEP (EQ X Y))) is a theorem.
[689 cns / .7 s + 0.0 gc + 0.0 io (= 1 @ 0)]
EQ
This conjecture can be simplified, using the abbreviations AND and
IMPLIES, to:
(IMPLIES (AND (OTM Y) (OZEROP Y))
(EQUAL Y (QUOTE (1QUOTE OZERO)))).
This simplifies, opening up the definition of OZEROP, to:
T.
Q.E.D.
This conjecture simplifies, expanding the definitions of OZEROP and LTE,
to:
T.
Q.E.D.
This formula can be simplified, using the abbreviations OZEROP, AND,
and IMPLIES, to:
(IMPLIES (AND (OZEROP Y)
(LTE X Y)
(NOT (EQUAL X (QUOTE (1QUOTE OZERO)))))
(NOT (OTM X))),
which simplifies, expanding the functions OZEROP and LTE, to:
T.
Q.E.D.
Name the conjecture *1.
Since there is nothing to induct upon, the proof has
************** F A I L E D **************
←PROVE.LEMMA(LTE.BI (REWRITE)
(IMPLIES (NOT (LTE X Y)) (LTE Y X))
NIL)
This formula can be simplified, using the abbreviations NOT and IMPLIES,
to:
(IMPLIES (NOT (LTE X Y)) (LTE Y X)),
which we will name *1.
Let us appeal to the induction principle. Four inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (OR (NOT (OZEROP Y))
(NOT (OZEROP X))))
(p Y X))
(IMPLIES (OZEROP X) (p Y X))
(IMPLIES (OZEROP Y) (p Y X))
(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(p (PB Y) X)
(p Y (PB X))
(p (PB Y) (PB X))
(p (PA X) (PA Y))
(p (PA Y) (PA X)))
(p Y X))).
The inequalities LT.ID.PB, LT.PA.PA, LT.PA.PA.x, LT.PB.ID, and LT.PB.PB
establish that the measure (OTM.SIZE.2 Y X) decreases according to the
well-founded function LESSP in the induction step of the scheme. The
above induction scheme generates 19 new goals:
Case 19.(IMPLIES (AND (NOT (OR (NOT (OZEROP Y))
(NOT (OZEROP X))))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, unfolding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 18.(IMPLIES (AND (OZEROP X) (NOT (LTE X Y)))
(LTE Y X)),
which we simplify, expanding the definitions of OZEROP and LTE, to:
T.
Case 17.(IMPLIES (AND (OZEROP Y) (NOT (LTE X Y)))
(LTE Y X)).
This simplifies, expanding the definitions of OZEROP and LTE, to:
T.
Case 16.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE (PB X) Y)
(LTE (PB X) (PB Y))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)),
which we simplify, unfolding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 15.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE (PB X) Y)
(LTE (PB X) (PB Y))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, expanding OZEROP, NOT, OR, and LTE, to:
T.
Case 14.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE Y (PB X))
(LTE (PB X) (PB Y))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, opening up OZEROP, NOT, OR, and LTE, to:
T.
Case 13.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE Y (PB X))
(LTE (PB X) (PB Y))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, expanding the functions OZEROP, NOT, OR, and LTE, to:
T.
Case 12.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE (PB X) Y)
(LTE (PB Y) (PB X))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, unfolding OZEROP, NOT, OR, and LTE, to:
T.
Case 11.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE (PB X) Y)
(LTE (PB Y) (PB X))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)),
which simplifies, opening up the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 10.(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE Y (PB X))
(LTE (PB Y) (PB X))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)),
which simplifies, expanding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 9. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE Y (PB X))
(LTE (PB Y) (PB X))
(LTE (PA Y) (PA X))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, expanding OZEROP, NOT, OR, and LTE, to:
T.
Case 8. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE (PB X) Y)
(LTE (PB X) (PB Y))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)),
which simplifies, unfolding the functions OZEROP, NOT, OR, and LTE,
to:
T.
Case 7. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE (PB X) Y)
(LTE (PB X) (PB Y))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)),
which simplifies, opening up the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 6. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE Y (PB X))
(LTE (PB X) (PB Y))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, unfolding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 5. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE Y (PB X))
(LTE (PB X) (PB Y))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)),
which we simplify, expanding the functions OZEROP, NOT, OR, and LTE,
to:
T.
Case 4. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE (PB X) Y)
(LTE (PB Y) (PB X))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, expanding OZEROP, NOT, OR, and LTE, to:
T.
Case 3. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE (PB X) Y)
(LTE (PB Y) (PB X))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, expanding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 2. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE X (PB Y))
(LTE Y (PB X))
(LTE (PB Y) (PB X))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)),
which simplifies, expanding the functions OZEROP, NOT, OR, and LTE,
to:
T.
Case 1. (IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(LTE (PB Y) X)
(LTE Y (PB X))
(LTE (PB Y) (PB X))
(LTE (PA X) (PA Y))
(NOT (LTE X Y)))
(LTE Y X)).
This simplifies, opening up the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
That finishes the proof of *1. Q.E.D.
[65003 cns / 44.4 s + 15.9 gc + 5.3 io (= 71 @ 1)]
LTE.BI
Name the conjecture *1.
Since there is nothing to induct upon, the proof has
************** F A I L E D **************
This formula can be simplified, using the abbreviation EQ, to:
(LTE X X),
which we will name *1.
Since there is nothing to induct upon, the proof has
************** F A I L E D **************
This formula can be simplified, using the abbreviations LT and NOT, to:
T,
which we simplify, clearly, to:
T.
Q.E.D.
This formula can be simplified, using the abbreviation IMPLIES, to:
(IMPLIES (OTM X) (LTE X X)),
which we will name *1.
Since there is nothing to induct upon, the proof has
************** F A I L E D **************
This formula can be simplified, using the abbreviation IMPLIES, to:
(IMPLIES (OTM X) (EQ X X)),
which simplifies, expanding the function EQ, to the new conjecture:
(IMPLIES (OTM X) (LTE X X)).
Give the above formula the name *1.
Since there is nothing to induct upon, the proof has
************** F A I L E D **************